from z3 import *


A = DeclareSort("A")
B = BoolSort()
R = Function("R", A, A, B)
TC_R = TransitiveClosure(R)
s = Solver()
a, b, c = Consts("a b c", A)
s.add(R(a, b))
s.add(R(b, c))
s.add(Not(TC_R(a, c)))
print(s.check())  # produces unsat
# > unsat
